X:(), y:( List). q-linear(0;j.X(j);y) = X(0) 

latex

Definitions	P & Q, x. t(x), T, P  Q, P  Q, True, False, P  Q, A, A  B, t  T, x(s), q-linear(k;i.X(i);y), , x:A. B(x), i  j < k, {i..j}, , S  T
Lemmas	mon ident q, qadd comm q, int inc rationals, sum unroll base q, true wf, squash wf, qadd wf, int seg wf, length wf1, select wf, qmul wf, le wf, nat wf, rationals wf